Technical Report for User Study

This document presents the full analysis of the User Study on the usability of LiquidJava.

To evaluate LiquidJava, we have developed a user study that combines the two types of tests to answer the following research questions:

The study was divided into X tasks, namely:

The study and its tasks was evaluated by a Ethics Commitee prior to its start, and all participants signed a participation agreement.

This study was designed to have 30 participants familiar with Java. Therefore, participants were recruited through social media channels, such as Twitter, Facebook and Instagram, and through direct contact via email.

The remaining of this document presents the results and the performed analysis.

Data

The study sessions were all conducted through the Zoom video platform, given the restrictions imposed by the COVID-19 pandemic, and the participants used their own environments to complete the study tasks.

The participants were given a study guide with the questions and the answer sheet all integrated into a Google Form. All the tasks and steps that the participants needed to take were included in the form to reduce the interviewer bias.

Therefore the data gathered joins the answers given by the participants with the time measured by the interviewer. The answers that were not in english were automatically translated using Google Translate, and are identified with an * at the end of the answer.

Participant's Background

When registering to the study, all participants answered questions about their familiarity with:

From all participants, 17 declared to be Very Familiar with Java, 11 are Familiar with the language, and 2 are Vaguely Familiar. These last group of participants were still selected to the study since they had already used test cases and testing frameworks in Java, which adds to the knowledge necessary to participate in the study.

The vast majority of participants had used test cases and Java testing frameworks before, as expected. And 90% of participants never had contact with LiquidJava. The ones that answered Yes to this question attended previous talks about the project but had never used the capacities of the tool while programming.

Participants that had contact with LiquidJava also considered themselves Familiar or Very Familiar with Refinement Types.

The interviewer also inquired about the occupation of the participants, and the results are in the following table.

Occupation/Job #Participants
Business 8 (26.7%)
Faculty 6 (20.0%)
PhD Students 5 (16.7%)
Master Students 7 (23.3%)
Final-Year Bachelor Students 4 (13.3%)

Exercises and Results

This section presents the exercises used in each of the tasks of the study and the results obtained.

Task 2

Interpreting Refinements without prior explanation

Since 90% of the participants had no previous contact with LiquidJava, and more than 80% were not familiar with Refinement Types, we wanted to understand if, without a prior explanation, the added specifications were intuitive to use. Thus, the study included a task with refinements examples that the participants needed to interpret and use in a correct and incorrect form. Specifically, we presented three code snippets with LiquidJava refinements with an increasing difficulty level and asked the participants to implement a correct and incorrect usage for each of the represented features.

Interpreting refinement in variable n the first exercise, participants had to assign a correct and incorrect value to the variable x, which restricted the range of values to the Earth's surface temperature limits.

// 1 - Variable Refinement
@Refinement("-25 <= x && x <= 45")
int r;

Interpreting refinement in Method The second exercise asked the participants to implement a correct and incorrect invocation of function1, where the second parameter depends on the first.

// 2 - Function/Method Refinement
@Refinement("_ >= 0")
public static double function1(@Refinement("a >= 0") double a, @Refinement("b >= a") double b){
  return (a + b)/2;
}

Interpreting refinements as state transitions in class Finally, the last task presented a class protocol with three possible states and methods that modeled the object state, and the participants were asked to create a MyObj object and implement a correct and incorrect sequence of at least three invocations. The MyObj class aimed to represent a Vending Machine object with the three states sX, sY and sZ as Show Items, Item Selected and Paid, respectively. The anonymization of the states and the class name were intentional to make the participants try to understand the refinements instead of calling the methods according to their mental idea of how a vending machine works.

@StateSet({"sX", "sY", "sZ"})
public class MyObj {

    @StateRefinement(to="sY(this)")
    public MyObj() {}

    @StateRefinement(from="sY(this)", to="sX(this)")
    public void select(int number) {}

    @StateRefinement(from="sX(this)", to="sZ(this)")
    public void pay(int account) {}

    @StateRefinement(from="sY(this)", to="sX(this)")
    @StateRefinement(from="sZ(this)", to="sX(this)")
    public void show() {}
}

The plot shows the evaluation of the answers given by the participants. Each answer was classified as Correct if both the correct and incorrect usage of the specification were correct, Incorrect if at least one of the usages was incorrect, or Unanswered if the placeholder for answering was left blank.

In the variable assignment, 86.7% of the participants answered correctly. The remaining participants understood the error when the examples were explained and claimed that the error was a pure distraction and misread the logical operators. The invocation of the annotated method had only one incorrect answer (3.3%). For the sequential methods' invocations, that depended on the class protocol described using the @StateRefinements, 46.7% of the answers were correct, and the remaining amount was split into incorrect and blank answers, showing that this example is less intuitive and harder to understand without a prior explanation, but still comprehensible by almost half of the participants.

Overall, refinement annotations in variables and methods are intuitive and easy to understand. However, the annotation of classes and their methods with protocols is less intuitive, and, in half of the cases, the participants would need a previous explanation to use these annotations correctly.

Task 1 & 3

Using Java and LiquidJava to Detect and Fix Bugs

This section joins the first and third tasks, both related to finding implementation errors in Java code with or without the help of refinements. The pair of tasks aim to validate if using Java with Liquid Types makes it easier and faster to detect and fix implementation errors in LiquidJava than in plain Java. To this end, we chose four exercises with implementation errors that the participants had to detect and fix. Firstly only using the plain Java code (Task 1: Find the error in plain Java) and then with the help of LiquidJava and its plugin for Visual Studio Code (Task 3 - Find the error in LiquidJava). Between both tasks, the participants had a small introduction to LiquidJava.

Each exercise had a plain Java version and a LiquidJava version with the same implementation errors to allow us to compare the number of participants that found and fixed the bug and the time taken in each version. The first group of participants started with exercises Sum and Socket while the second group started with the plain Java versions of the exercises Fibonacci and ArrayDeque. When moving to detect the errors using LiquidJava, the first group had the exercises Fibonacci and ArrayDeque whereas the second group got the exercises Sum and Socket. Therefore, one participant never used the same exercise in both tasks, avoiding tainting the second task with previous knowledge of the solution and allowing us to obtain plain Java baselines for every exercise. With this split, the maximum number of answers to each version is 15 since only half the participants viewed each exercise version.

In both Task 1 and Task 3, we gathered the time spent in each exercise and the given answers. The answers were then evaluated into one of four possible categories: Correct, Incorrect, Unanswered, and Compiler Correct. The last category, Compiler Correct, represents the answers that, despite not having any error detected by the LiquidJava compiler, are not utterly correct according to the exercise.

Sum Exercise

The sum exercise contains a recursive method that should implement the sum of all numbers between 0 and the given parameter. However, it contains a bug in the base case since the method returns 0 if the gotten parameter is 1. This exercise was inspired by the recursion example presented in Refinement Types: A Tutorial.

Java version

public class Test2 {
    /**
    * The sum of all numbers between 0 and n
    * @param n
    * @return a positive value that represents the sum of all numbers between 0 and n, or 0 if n is negative
    */
    public static int sum(int n) {
        if(n <= 1)///correct: (n < 1) or (n <= 0)
            return 0;
        else {
            int t1 = sum(n-1);
            return n + t1;
        }
    }

}

LiquidJava version Since the informal documentation does not specify any conditions to the parameter its refinement is omitted. However, it specifies the return conditions that can be simplified into the return refinement presented, using the same expression as the tutorial.

@RefinementAlias("Nat(int x) {x >= 0}")
public class Test2 {
    /**
    * The sum of all numbers between 0 and n
    * @param n
    * @return a positive value that represents the sum of all numbers between 0 and n, or 0 if n is negative
    */
    @Refinement("Nat(_) && _ >= n")
    public static int sum(int n) {
        if(n <= 1)//correct: (n < 1) or (n <= 0)
            return 0;
        else {
            int t1 = sum(n-1);
            return n + t1;
        }
    }

}

It is possible to see that in the plain Java version, only one participant could not find and fix the bug, while the 14 others were able to find the error, and 13 correctly fixed it. On the other hand, in the LiquidJava version, every participant was able to locate the error. However, only 7 participants were able to fix it correctly, and the same number answered with Compiler Correct options.

The answers accepted as Correct adjusted the base case to one of the following versions: if(n <= 0) or if(n < 1). The answers considered Compiler Correct are the ones that silenced the compiler error but are not correct according to the informal specification. Among these answers, 6 out of the 7 participants changed the base case's return value, changing it to return 1, while the other participant answered return Math.abs(n).

The 46.7% of Compiler Correct answers suggests that the participants were more focused on silencing the compiler error than on correcting the program according to the informal specification. Additionally, we may relate the 40% of return 1 answers with the Task 1 of these participants, which included the Fibonacci exercise where the correct fix was changing the return line to return 1. This line of thought might indicate that the participants were biased by the previous sections of the study and opted for the same answer as they used in the beginning.

Sum Time

The time plot contains two similar distributions, with a shorter average time in the LiquidJava version. In minutes, the participants spent 4 minutes and 30 seconds on average finding and fixing the error in plain Java, whereas in LiquidJava, they spent an average of 3 minutes and 32 seconds, being faster by almost 1 minute.

Fibonacci Exercise

This exercise presents a recursive implementation of the method fibonacci that computes the nth Fibonacci number. However, the code contains an implementation error in the base case of the recursion, where the starting values of F(0) = 1 and F(1) = 1 are not respected.

Both versions of code are presented bellow.

Java code version:

public class Test2 {
    /**
    * Computes the fibonacci of index n
    * @param n The index of the required fibonnaci number
    * @return The fibonacci nth number. The fibonacci sequence follows the formula Fn = Fn-1 + Fn-2 and has the starting values of F0 = 1 and F1 = 1 
    */
    public static int fibonacci(int n){
        if(n <= 1)
            return 0;//correct: change to 1
        else
            return fibonacci(n-1) + fibonacci(n-2);
    }
}

LiquidJava code version:

@RefinementAlias("GreaterEqualThan(int x, int y) {x >= y}")
public class Test2 {
    /**
    * Computes the fibonacci of index n
    * @param n The index of the required fibonnaci number
    * @return The fibonacci nth number. The fibonacci sequence follows the formula Fn = Fn-1 + Fn-2 and has the starting values of F0 = 1 and F1 = 1 
    */
    @Refinement( "_ >= 1 && GreaterEqualThan(_, n)")
    public static int fibonacci(@Refinement("Nat(n)") int n){
        if(n <= 1)
            return 0;//correct: change to 1
        else
            return fibonacci(n-1) + fibonacci(n-2);
    }
}

Fib Time

We can see that all the participants could find and fix the exercise in LiquidJava, whereas in plain Java, only 73,3\% found the error, and 66,7\% were able to fix it.
The answers accepted as Correct changed the return of the base case to return 1, and all the different answers were determined as incorrect since they did not fix the presented error. Additionally, in plain Java, 2 participants in total decided to skip this question without answering the possible location of the bug or proposing a fix.

The time spent on the Java version was, on average, smaller than the time spent in LiquidJava. The average time spent in the plain Java exercise was 2 minutes and 52 seconds, while the time spent on LiquidJava was 3 minutes and 22 seconds, reaching a difference of 30 seconds. This result suggests that participants are already used to Fibonacci's plain implementation given its popularity. When the new refinements were added, participants spent more time understanding the different sections of the code.

Socket

This exercise uses the Socket class from the external library java.net. The class was modeled with states and state transitions according to the informal documentation of the class and a client method createSocket(...) was created with incorrect usage of the invocations' order. In this exercise, the error lies in the invocation of socket.sendUrgentData(90) before the socket is connected to a server.

Java version

public class Test2 {

    public void createSocket(InetSocketAddress addr) throws IOException{
        int port = 5000;
        InetAddress inetAddress = InetAddress.getByName("localhost");    

        Socket socket = new Socket();
        socket.bind(new InetSocketAddress(inetAddress, port));
        socket.sendUrgentData(90);
        socket.close();
    }
}

The same client code was shown to participants in both Tasks 1 and 3. However, the code in Task 3 contained a file with the Socket class annotations of states and the allowed state transitions between the methods. Again, the informal documentation of the class from the library could be reached using the enabled Java plugin.

LiquidJava - External Refinements

@ExternalRefinementsFor("java.net.Socket")
@StateSet({"unconnected", "binded", "connected", "closed"})
public interface SocketRefinements {

    @StateRefinement(to="unconnected(this)")
    public void Socket();

    @StateRefinement(from="unconnected(this)",to="binded(this)")
    public void bind(SocketAddress add);

    @StateRefinement(from="binded(this)", to="connected(this)")
    public void connect(SocketAddress add);

    @StateRefinement(from="binded(this)", to="connected(this)")
    public void connect(SocketAddress add, int timeout);

    @StateRefinement(from="connected(this)")
    public void sendUrgentData(int n);

    @StateRefinement(to="closed(this)")
    public void close();
}

Socket Time

ArrayDeque

This exercise presented a program that uses the ArrayDeque class from the java.util library. The class contains popular methods to add, remove, and retrieve elements from an ArrayDeque object. These operations may depend on the number of elements present on the deque, and if those dependencies are not respected, exceptions will arise. With the Java plugin enabled on the IDE, participants were able to access the documentation of the class.

The exercise presents a program that includes sequential invocations of methods of ArrayDeque. However, the invocation p.getLast() on line 8 produces an exception since it is called when the object is empty.

Java version

public class Test2 {

    public static void main(String[] args) throws IOException{
        ArrayDeque<Integer> p = new ArrayDeque<>();
        p.add(2);
        p.remove();
        p.offerFirst(6);
        p.getLast();
        p.remove();
        p.getLast();
        p.add(78);
        p.add(8);
        p.getFirst();

    }

}

The code presented in the LiquidJava version, includes the client as before, and also a separate file with the modelling of ArrayDeque with the ghost variable size.

LiquidJava version - External Refinements

@ExternalRefinementsFor("java.util.ArrayDeque")
@Ghost("int size")
public interface ArrayDequeRefinements<E> {

    public void ArrayDeque();

    @StateRefinement(to="size(this) == (size(old(this)) + 1)")
    public boolean add(E elem);

    @StateRefinement(to="size(this) == (size(old(this)) + 1)")
    public boolean offerFirst(E elem);

    @StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))")
    public E getFirst();

    @StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))")
    public E getLast();

    @StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)")
    public void remove();

    @StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)")
    public E pop();

    @Refinement("_ == size(this)")
    public int size();

    @Refinement("_ == (size(this) <= 0)")
    public boolean isEmpty();

}

Deque Time

All the participants could correctly find and fix the error in both plain Java and LiquidJava. There were multiple options to fix the code to prevent the raising of the exception; the accepted answers included removing p.getLast() on line 8, verifying if the queue is empty with if(!p.isEmpty) right before line 8, changing the line to p.peekLast(), among others.

The average time participants took in this exercise in LiquidJava (2 minutes and 56 seconds) was 45 seconds less than using plain Java (3 minutes and 41 seconds).

Discussion on Java and LiquidJava exercises

With the results gathered from Task 1 and Task 3, we can conclude that LiquidJava helped the participants find the bugs present in the code since the percentage of participants who found the bugs was always higher, or equal, in the LiquidJava version when compared to the plain Java version. LiquidJava also helped the participants fix the bugs according to the error information provided. However, the participants focused on silencing the errors, which led to some answers that were only considered Compiler Correct since the error was not totally fixed.

The task of finding and fixing the bugs was faster in LiquidJava in all but one exercise. The latter refers to the Fibonacci example, which may have had a shorter time because of its popularity and the fact that most developers are familiar with its plain Java version. From all the exercises, the one that benefited the most from the LiquidJava version was the Socket client, where we moved from having only one participant finding the error in plain Java to 100% in LiquidJava, and from no participant fixing the bug to 100% fixing it. These percentages may indicate that LiquidJava is more useful when used in more complex programs, with classes that have protocols less-known by developers.

Overall, LiquidJava helped participants find and fix the bugs, and in some cases, it helped them do it faster.

Instalation of LiquidJava

We inquired the participants on the ease of intalling the plugin. The majority felt that it was very easy to install the plugin (5 band).

The 3 empty answers were from participants that used the interviewer's environment to complete the tasks due to one of two problems:

The participant that rated the installation 3, did not have the code command in terminal.

Task 4

Annotate with LiquidJava

In this task participants were asked to add LiquidJava annotations to the implemented code according to the informal documentation written in the program as comments. In this step, participants could use the website and the video to help writing the refinements.

Participants had to annotate programs with increasing order of difficulty. The first program relied only on the annotation of a variable with its bounds. The second program expected the annotation of a method by specifying the parameters and return refinements. Finally, the third program required the annotation of a class protocol and the class fields. For each program, we presented an example of a correct usage of the refinement and another example of its incorrect usage to help the developers test their refinements.

The participants shared their proposals for the annotation of each exercise, and we evaluated them with the four categories used in the previous section, of Correct, Incorrect, Unanswered and Compiler Correct.

There were three code snipets presented to the participants related to each of the exercises. The results are shown below.

Variable Annotation

/* A month needs to have a value between 1 and 12*/
int currentMonth;   

currentMonth = 13; // Error
currentMonth = 5;  // Correct

The first and more straightforward program is the annotation of a variable within a upper and lower bound. This would be accomplished with the annotation: @Refinement("currentMonth >= 1 && currentMonth <= 12 "). In the first exercise, all the participants used the website as a resource to look for the right syntax, and 100% of them annotated the variable correctly.

Method Annotation

/**
* Returns a value within the range
* @param a The minimum border
* @param b The maximum border, greater than a
* @return A value in the interval [a, b] (including the border values)
*/
public static int inRange(int a, int b) {
    return a + 1;
}
...
inRange(10, 11); //Correct
inRange(10, 9); //Error

The method presented in the second exercise where participants should add a refinement to the second parameter, changing the signature of the method to public static int inRange(int a, @Refinement("b > a") int b), and refine the return type of the method, adding the refinement @Refinement("_ >= a && _ <= b") above the method's signature.

24 out of 30 participants were able to add the expected annotations leading to 80% of Correct answers. However, 20% only added the annotations to the parameter, silencing the example error but not completing the exercise in its totality, which lead to the Compiler Correct answers.

Class Annotation

public class TrafficLight {
  private int r;    
  private int g;    
  private int b;

  public TrafficLight() { r = 76; g = 187; b = 23; }
  public void transitionToGreen() { r = 76; g = 187; b = 23; }
  public void transitionToAmber() { r = 255; g = 120; b = 0; }
  public void transitionToRed() { r = 230; g = 0; b = -1; }
}

//Correct Test - different file
TrafficLight tl = new TrafficLight();
tl.transitionToAmber();
tl.transitionToRed();
tl.transitionToGreen();
tl.transitionToAmber();

//Incorrect Test - different file
TrafficLight tl = new TrafficLight();
tl.transitionToAmber();
tl.transitionToRed();
tl.transitionToAmber();
tl.transitionToGreen();

For the last exercise we asked participants to "Annotate the class TrafficLight, that uses rgb values (between 0 and 255) to define the color of the light, and follows the protocol defined by the image [below]", as announced in the study guide. The evaluation of this exercise was split into two: the addition of the refinements to model the class protocol, and the specification on the class private fields.

Deque Time

100% of the participants correctly modeled the class by declaring the starting states and the state transitions allowed in each method. This percentage constitutes a significant increase in the understanding of the class protocols when compared to the first time participants tried to understand the protocol in Task 1, where half of the participants could not interpret the meaning of the annotations.

However, only 43.3% of the participants annotated the class fields, and the remaining participants did not add any refinement to them, leaving an incorrect assignment in the body of one class method. There might be several reasons for why participants did not annotate the class fields. A possible explanation is that they misinterpreted the exercise, not realising the need for these annotations, another possible explanation is that participants did not consider it important to add these annotations to the code.

How easy was the annotation

After being introduced to the annotations, the participants had to evaluate the ease of adding annotations from 0 - Very Difficult to 5 - Very Easy. 60% of the participants considered that adding the annotations was Very Easy, while the remaining 40% considered the task Easy, leading us to conclude that the refinements are simple to add to implemented code.

Comments

At the end of the tasks, we asked the participants about the overall experience of using LiquidJava using three questions:

The answers to each question were analysed using a qualitative coding approach. We used inductive coding to create the codes, which were then used to review all passages and to identify the main topics of each answer, leading to a cohesive and systematic view of the results.

What did you enjoy the most about LiquidJava?

About the aspects that participants enjoyed about LiquidJava, we found that participants mostly appreciated the error reporting, using state refinements to model objects and the intuitive and non-intrusive syntax.

The codes used and examples of the participants answers related to the codes are presented below.

Codes representing the answers

  1. Error Reporting

    • The fact it reported un-compliances with the specifications
    • refinement types we have an assurance that the program is logically consistent at the time of coding.
    • Helps to define the program's logic and avoid future errors

  2. State Refinements

    • Everything, a particular note on the staterefinement it is very useful
    • Specification of states, because enforcing correct state transitions in the implementations is tedious and error-prone

  3. Syntax

    • The simple syntax based on annotations
    • Very intuitive syntax
    • non-intrusive

  4. Plugin

    • Excellent integration with VSCode
    • Very well assisted by the custom vs code extension

  5. Understandability

    • Very intuitive
    • Easy to understand in terms of semantics

  6. Useful

    • Highly useful
    • It helped me a lot to known which values/methods are correct when I'm coding

  7. Resources

    • Using the video and the examples it was easy to understand how the refinements work
    • The examples and the video were very illucidative

  8. Flexibility

    • I liked the flexibility of scenarios in which I could use LiquidJava
    • +1 to the diverse set of refinements that can be written in different parts of the code

What did you dislike the most about LiquidJava?

To the question of the LiquidJava aspects that participants disliked, only 26 participants reported answer. The remaining 4 participants did not identify any negative aspect, leaving the answering slot empty.

Of the 26 answers, 8 explicitly mentioned there was Nothing they did not like. The remaining negative aspects were about the syntax and some plugin features.

Codes representing the answers

  1. Noting (8) - "Nothing, it is quite straightforward to be used"

  2. Syntax (6)- "[in the state refinement] repetition of this", "the usage of _ for the return value"

  3. Plugin (4) - "Improve the usability of the plugin -remove double quotes; - use auto-complete inside the refinements", "not being able to correct multiple files at the same time"

  4. Not Intuitive (3)- "Hard to understand without access to documentation, mainly DFA protocols"

  5. Error Messages(3) - "Some error messages are not straight to the point"

  6. Verbose (3) -"Makes Java more verbose"

  7. Other (2) -"The state transition is a bit harder to get but paired with the given documentation is fine.", "The installation process was not very user friendly"

Would use LiquidJava in projects

The last question of the study asked the participants if they would use LiquidJava in their projects, to which all the participants answered affirmatively. However, in the final suggestions, one participant declared that they would only use it in critical parts of the project, and two other participants stated that they are not currently using Java in any project but would like to have similar verifications in other programming languages.

Study Conclusions

The major takeaways of the study can be summarized in the following points.